Tute (Week 8)

There's many ways to do this. Here's one.

Let \(K\) and \(V\) denote the sets of keys and values, respectively.

The state is a set of local states for each DBMP, where each DBMP has

• A PID \(\in \mathbb{N}\)
• A local clock value \(\in \mathbb{N}\)
• A database \(db\), which is a function \(K \rightarrow V \times (\mathbb{N} \times \mathbb{N})\)
• A list of incoming messages \(\in \mathsf{List}(K \times V \times (\mathbb{N} \times \mathbb{N}))\). (Let's not worry about how to formalise lists in set theory here).

The incoming messages aren't physically part of the DBMP, of course — they're out there in the network somewhere. Nonetheless, it's convenient to model it as a queue.

Then, in our labelled transition system \((S,\rightarrow)\) we have \[ S = \mathcal{P}(\mathbb{N} \times \mathbb{N} \times (K \rightarrow V \times (\mathbb{N} \times \mathbb{N})) \times \mathsf{List}(K \times V \times (\mathbb{N} \times \mathbb{N}))) \]

This model comes with some caveats. For example, we don't want \(S\) to contain more than one element with the same PID, but we haven't forbidden it. To achieve this, we could phrase \(S\) as a partial function from PIDs instead.

We'll define the transition relation using the following inference rules.

The first inference rule represents a DBMP receiving, and accepting, a modification request:

\[ \dfrac{db(k) = (v',(ck'',pid'')) \quad (ck'',pid'') < (ck',pid') \quad \forall p \in procs. pid \neq p_1 }{(pid,ck,db,(k,v,(ck',pid'))::msgs) \cup procs \longrightarrow (pid,ck+1,db[k \mapsto (v,(ck',pid'))],msgs) \cup procs } \]

The next inference rule represents a process rejecting a modification request:

\[ \dfrac{db(k) = (v',(ck'',pid'')) \quad (ck'',pid'') > (ck',pid') \quad \forall p \in procs. pid \neq p_1 }{(pid,ck,db,(k,v,(ck',pid'))::msgs) \cup procs \longrightarrow (pid,ck+1,db,msgs) \cup procs } \]

The final inference rule represents a process creating a modification request:

\[ \dfrac{ }{(pid,ck,db,msgs) \cup procs \longrightarrow (pid,ck+1,db,msgs + [(k,v,(ck,pid))]) \cup \{(pid,ck,db,msgs + [(k,v,(ck,pid))]) : (pid,ck,db,msgs) \in procs\} } \]

Note that this rule doesn't actually perform the local update, instead it sends the modification request to itself as well as to all the other processes. This is a deliberate simplification, to avoid having two inference rules doing essentially the same work.

There is one more aspect not captured by these inference rules: the rules for accepting and rejecting requests always take the first (oldest) element from the message list. However, it's possible for a message other than the oldest to arrive first, if its DBMP of origin is different. To model this, we would have to allow messages to be consumed from not just the first element in the list, under certain circumstances.

In the above, \(+\) denotes list append, and \(::\) denotes list cons (inserting an element to the front of a list).

For one thing, the summary above only considers modification requests originating from what the RFC calls assignments. Selection, creation and deletion requests are completely ignored.

As for ambiguities, consider the following quote:

"When the assignment is initiated (by a person or process) the DBMP involved makes the change locally, and creates a copy of the modified entry and an associated list of DBMPs to which the change must be sent."

When that says "make the change locally", does it mean make the change no matter what? Or does it mean make the change, unless the entry we already have has a higher timestamp?

We chose the latter for a number of reasons.

1. The algorithm doesn't satisfy eventual consistency if timestamps are ignored for local updates: a DMBP may then make a local update that every other process rejects.

2. The following quote comes later, and seems to suggest interpretation 2:

   "When a DBMP receives an assignment modification (either locally or from another DBMP) it compares the timestamp of the modification with the timestamp of the copy of the entry in its database and keeps whichever is more "recent" as defined by the ordering given above"

   That quote suggests, but doesn't make 100% clear, that interpretation #2 is intented depending on what exactly is meant by a local modification.

Another point: a literal reading of the text seems to suggest modification requests are always sent out when a local update is attempted, even one that will clearly be rejected because the DBMP of origin already had a more recent entry. That's what we went with. But there are at least two other readings possible:

1. Modification requests are only sent to others if it would have a higher timestamp than the existing entry in our local database, i.e., if our local update would succeed.
2. If a local modification fails, an update is still sent to others— but with the existing entry in our databse, not with our proposed modification.

If two modification requests \((k,v,(n,pid))\) and \((k',v',(n,pid))\) have equal timestamps, then (because PIDs are unique) they must originate from the same DBMP. Because clocks are incremented with every action performed, the two requests must also originate with the same action. The only action that sends messages is clause 4 above, which sends identical messages.

The invariant can be stated something like this. For every key \(k\) there is a unique \(v\) associated with the lexicographically highest timestamp \(ts\) of a message or database entry involving \(k\). For every DBMP i that does not have \((v,ts)\) associated with \(k\), there is an in-flight message to \(i\) containing the modification request \((k,v,ts)\).

If there are no in-flight messages, this invariant implies that every DBMP must have identical databases. Proof by contradiction: if not, there must a DBMP that has an entry with a lower timestamp than the maximum for some key \(k\). This DBMP must have an inbound modification request, which contradicts the invariant.

It remains to show that the invariant is preserved by actions 4 and 5, which is relatively straightforward.

Suppose there are three DBMPs with PIDs 0, 1 and 2. Initially they all map the key \(k\) to the value `"hi"`. Then consider the following interleaving:

1. DBMP \(0\) sends request \((k,\mbox{`hi`},(5,0))\), and increments its clock value from \(5\) to \(6\).
2. DBMP \(1\) and \(2\) receive this message from \(0\), and update their local databases accordingly.
3. DBMP \(1\) sends request \((k,\mbox{`hej`},(3,1))\), and increments its clock value from \(3\) to \(4\).
4. DBMP \(2\) receives \((k,\mbox{`hej`},(3,1))\), and discards the update because \(3 < 5\).

This is causally inconsistent because, even though the out-of-synch clocks say otherwise, the modification request from DBMP \(1\) demonstrably happens after that of DBMP \(0\). Since sending of the former precedes receipt of the latter, there may even be a direct causal link. It could be that DBMP \(1\) decided to send its request only because of the request it received from DBMP \(0\).

If you're interested in how to think about causality in distributed systems, and how to set up the clocks so that they respect causality, the canonical reference is Leslie Lamport. But that's beyond the scope of the course.